COMMENT ⊗   VALID 00016 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	LSPCLT.DIR[LSP,CLT] is an annotated directory of files on [LSP,CLT].
C00004 00003	22-Aug-78  1353(partial up date)
C00012 00004	PUBBING conventions
C00014 00005	To pub individual chapters: 
C00015 00006	Plan of action w78
C00017 00007	General improvements for text
C00019 00008	Random ideas
C00020 00009	Work to do (file handling, form, ...):
C00021 00010	Work to do (examples programs ...)
C00022 00011	Work to do ( theoretical):
C00023 00012	Proposed (revised) organization of Book
C00026 00013	Ideas for contents of additional chapters:
C00029 00014	Notes and comments.
C00030 00015	Interesting data structures.
C00031 00016	Project and program ideas
C00035 ENDMK
C⊗;
;LSPCLT.DIR[LSP,CLT] is an annotated directory of files on [LSP,CLT].
If it has disappeared or is out of date type DO MKDIR.DO[LSP,CLT] to the monitor
    and an new directory will be made.
(Directory of old versions of book are in 206LSP.ARC[206,LSP])
22-Aug-78  1353(partial up date)

Filnam Ext   PPN    Size  Written  Time Pro    Writer     Reference      Dumped      Off

BOOK   XGP 206LSP  138.3 25-Sep-78 0613 000 LISHAR PUB2   05-Dec-78 22-Oct-78 P1246>
	F78 version of BOOK, now deleted.

BOOK       LSPCLT    3.2 22-Aug-78 1656 005   1CLT E      
	Documentation and ideas file

****Pubmacro files

BKMAC  PUB LSPCLT    2.0 22-Mar-78 0122 000   1CLT E      22-May-78 04-Apr-78 P1101>
LSPMAC PUB LSPCLT    1.8 26-Apr-78 0956 005   1CLT E      15-Jun-78 09-May-78 P1126>

LSPEXP PUB LSPCLT    3.0 20-Mar-78 2302 005   1CLT E      20-Mar-78 04-Apr-78 P1101>
	Pub test file

****Assembly files

LSPDOC PUB LSPCLT    640 21-Mar-78 0453 005   1CLT E      31-May-78 04-Apr-78 P1101>
	Onesided
LSPDC1 PUB LSPCLT    512 21-Mar-78 0451 000   1CLT E      31-Mar-78 04-Apr-78 P1101>
	Twosided

****Batching (see p4)

MKCHAP DO  LSPCLT    256 26-Jul-78 0009 000   1CLT E      26-Jul-78

   do mkchap (answer time+2min to T=	and <chapter name> to C=	)
	this will do the relevant pub job in batch mode 
	and write the xgp file on [BOO,JMC]

****Text

PREFAC[BOO,JMC]   1.1 25-Jul-78 2312 000   1CLT E      31-Jul-78 09-Aug-78 P1185>
    Introduction

READIN[BOO,JMC]  15.6 22-Aug-78 0344 000   1CLT E      22-Aug-78
	Introduction to LISP:  S-expressions, LISP program constructs, 
	how to write recursive function definitions,EVAL


WRITIN[BOO,JMC]  10.1 11-Aug-78 0445 005   1CLT E      12-Aug-78 20-Aug-78 P1194
    Forms of recursion and examples, thinking (reasoning) about recursive programs,
	induction,  informal proofs.

PROVIN[BOO,JMC]  20.1 12-Aug-78 1906 000   1CLT E      12-Aug-78 20-Aug-78 P1194
	Proving Properties of LISP programs: 
	First order theory of LISP and example proofs

PROVEX[BOO,JMC] 
	Proving Properties of LISP programs: 
	First order theory of LISP and example proofs

IMPURE[BOO,JMC]   7.6 08-Aug-78 2009 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
	Impure and Unclean LISP:
	PROGs and Arrays, RPLACs, Property lists, Atom and pname manipulation

MACHIN[BOO,JMC]
	How LISP works: Oblists,gc,i/o,errors,tracing,debugging,editing

SEARCH[BOO,JMC]   9.3 31-Jul-78 1351 005   1CLT E      08-Aug-78 13-Aug-78 P1190>
    Tree searching (depth first: puzz,  breadth first: graph min dist or csg)
    Game tree searching: αβ  TIC TAC TOE

EXTEND[BOO,JMC]   4.6 08-Aug-78 2013 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
	Transforming LISP programs.
	Purifying progs, derived programs, (a little metatheory?).
    
ABSNTX[BOO,JMC]   7.5 08-Aug-78 2015 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
    Description of abstract syntax: synthetic,analytic,relations,induction
	(extract abstract syntax of S-expressions from LISP axioms as example.)
	defining semantics of programs,	proving compiler correctness(MCPAIN)

COMPIL[BOO,JMC]   8.0 31-Jul-78 1216 005   1CLT E      19-Aug-78 13-Aug-78 P1190>
	Compling (LISP programs) in LISP :   LAP,LCOM0,LCOM4

COMPUT[BOO,JMC]   2.3 08-Aug-78 2016 005   1CLT E      08-Aug-78 20-Aug-78 P1194>
	Computability and Noncomputability  


LSPBIB[BOO,JMC]   1.0 22-Mar-78 0303 005   1CLT E      22-Mar-78 04-Apr-78 P1101>
	Bibliography, partially annotated


****Appendices

FOLAPX[BOO,JMC]   9.2 22-Mar-78 0304 005   1CLT E      31-Mar-78 04-Apr-78 P1101>
    Appendix containing FOL proofs

LCOMAP[BOO,JMC]   2.8 20-Mar-78 0250 005   1CLT E      22-Mar-78 04-Apr-78 P1101>
    Appendix containing internal forms of LCOM0 and LCOM4

****Pub files: pub commands for pubbing individual chapters.

PREFAC PUB LSPCLT    256 25-Jul-78 2312 000   1CLT E      31-Jul-78 09-Aug-78 P1185>

READIN PUB LSPCLT    512 12-Aug-78 1700 000   1CLT E      12-Aug-78 20-Aug-78 P1194
WRITIN PUB LSPCLT    768 12-Aug-78 1832 000   1CLT E      12-Aug-78 20-Aug-78 P1194
PROVIN PUB LSPCLT    512 12-Aug-78 1839 000   1CLT E      12-Aug-78 20-Aug-78 P1194
PROVEX PUB LSPCLT    
IMPURE PUB LSPCLT    256 08-Aug-78 2010 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
MACHIN PUB LSPCLT
SEARCH PUB LSPCLT    256 08-Aug-78 2012 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
EXTEND PUB LSPCLT    384 08-Aug-78 2013 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
ABSNTX PUB LSPCLT    256 08-Aug-78 2014 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
COMPIL PUB LSPCLT    256 08-Aug-78 2011 000   1CLT E      08-Aug-78 20-Aug-78 P1194>
COMPUT PUB LSPCLT    256 08-Aug-78 2017 000   1CLT E      08-Aug-78 20-Aug-78 P1194>

LSPBIB PUB LSPCLT    256 26-Jul-78 0008 000   1CLT E      31-Jul-78 09-Aug-78 P1185>

	PUB <chapter name> pubs the appropriate chapter; alias to lsp,clt first


****Micsellaneous

EXCISE     LSPCLT    4.8 01-Aug-78 2031 000   1CLT E      01-Aug-78 13-Aug-78 P1190>
	Hunks of text that have been excised but are worth keeping for later use.

	Total= 106.5


PUBBING conventions


BKMAC.PUB[BOO,JMC] and LSPMAC.PUB[BOO,JMC] have been modified as follows:
the fonts 8,A,B have been combined into one file denoted by 8 and 
attached to symb30.fnt[fnt,clt].  The symbols in this file are sized to
be compatible with grk30 (ht 32, ht above base line 27) and are as follows
fhtwxyzFPSY (from GRK30 as is)
@←c[ms25] circle-c
≤←b[math30] Scott po symbol
|←T[math30] Scott bottom symbol (qb or qw response)
*←*[math30] centered dot used for times  (q* response)
#←x[math30] raised "x" used for cross-product
&←I[math30] integral sign
∞←A[ms30] section sign   (qsect response)
π←π[math30] ¬ε symbol
:←:[zero30] umlaut
/← [brce35] upper corner trimmed to 32
{← [brce35] left brace trimmed to 32
\← [brce35] lower corner trimmed to 32
macros using the 8 or A fonts have been updated.

Figure response now always centers, takes a caption, end by "!"
Table response like figure.

sections and subsections have labels
To pub individual chapters: 

al lsp,clt
pub <chapter name>
; <chapter name> ε {PREFAC READIN WRITIN PROVIN IMPURE SEARCH
;		    EXTEND ABSNTX COMPIL COMPUT LSPBIB}


;or

do mkchap[BOO,JMC]
T=	<current time+2min or so>
C=	<chapter name>

;will create a batch job to do the above


;To pub book use LSPDOC.PUB (for 1 sided) or LSPDC1.PUB (for 2 sided)
;NB:  no guarantees as to uptodateness of these files
Plan of action w78

⊗(1)	Finish chapter I. Settle on form, notation conventions, etc.
⊗(2)	Update chapter II to conform to these conventions.
⊗(3)	Insert McPain into the Abstract Syntax chapter.
⊗(4)	Work out Impure Chapter
?(5)	Rewrite chapter III
(6)     Add chapter on Program transformations.
⊗(7)    Move eval into Chapter I
⊗(8)     Add normaliztion of conditionals as exercise to ABSNTX

hopefully all of this can be done before notes are pubbed for s78 class

Plan of action e78

⊗(1) Take care of bugs and improvements noted in S78 notes.

⊗(2) CH I: improvements as noted on content page.

⊗(3) CH II

⊗(4) CH III

⊗(5) CH IV  new title: Additional sections as noted on content page

⊗(6) Search chapter:  improvements as note on content page

⊗(7) Figure titles

(8) Index on definitions and important concepts



General improvements for text

Exercises:  Each chapter should have 
	simple and straight forward exercises at the end of most sections
	At the end of each chapter have a section of substantial exercises
	    relevant to the material in the chapter.
	Need to collect many more of each kind and improve those given

formulas or formulae??

Index on definitions (of programs)

Index of important concepts

Summary of axioms and theroems

Notation and symbols summary  formal conection between programs and terms.

switch names on definitions of reverse makin the efficient one reverse1

switch to symbolic labels for function defintions axioms, theorems etc.

Complete change of lisp term notation =→qequal, ∧ qand etc.

do we need subsubsections? probably in PROVIN any way.

Random ideas

Efficiency of programs:
	total number of conses vs amount of space needed at any one time.
	efficient version of subst

Simplification

Production rule programming

Transformations

Data directed version of LCOM
Production rule version of LCOM
More passes
Work to do (file handling, form, ...):

Finnish Pruning 206 files
    Document naming conventions etc.
    Get any relevant files from 206,CCG 
    Send notes to jmc ccg about documentation etc.

Fix function library
	Translate any interesting rlisp programs
	Document programs
	Get any inteesting function definitions from 206,ccg

Make maclisp file of all functions defined in book.

CCG has catalogue of lisp exercises according concepts required, done by avra cohn
	in his office (ici).  Take a look at this soon.


Work to do (examples programs ...)

Valmax/min Linemax/min Treemax/min  ??proof and cutoff

Clean

Mini scheme

implement LIT

Spruce up and document BB 
    (use for example of data driven computation, top level control, i/o )
     Include pp for lisp terms as S-exp?
     general method of specifying doc processor decorations

Modify LCOM4 to produce iterative code when possible
Modify LCOM4 to compile mapping functions


Work to do ( theoretical):

work out description of Ordinals, cantor normal form, ... 
	exercise: repn as sexp, order predicate, equality (of ord represented),
		  test for 0, succ, lim ord
	prove some properties of repn and functions
	natural arith
	ordinal arith

Program specification

Proving facts about functionals
    mapping functions for example
    proving things about the function defined by a SCHEME LABELS construct
    proving things about the function defined by a MACLISP LABELS construct

Proposed (revised) organization of Book

The idea is to divide the book in two parts (conceptually if not actually).
Part 1 covers the basic topics which would be the core of the course material.
Part 2 is a collection of special topics, more advanced material, examples
of programs and additional theoretical techniques....
For text book purposes material from part 2 could be selected according 
to taste and interest of teacher and students.

Part 1:

   I	Reading  LISP programs (function definitions)

  II	Writing  LISP programs

 III 	Proving statements about LISP programs

  IV 	Non trivial proof examples 

   V	Dynamic LISP --- prog, rplacs, etc. 

   Va	Extended methods of representation and proof: elephant, EXTEND

  VI	LISP implementation (how it really works)


Part 2:

SEARCH	Searching programs

EXTEND	Transforming LISP programs: move derived program feature to Va?

ABSNTX	Abstract Syntax omit?

COMPIL  The LCOM compilers theme and variations.

COMPUT	Computatibility/Non-computability

       	Control Structures

      	Pattern matching, syntax directed computation, data driven computation

	Dialects of LISP, systems written in LISP

	Collection of substantial programming and/or proving projects

Remarks:  Chapters with names exist is some form those with out names do not.

For more details on contents of chapters see LSPCMT[BOO,JMC]/11p and /12p.
Ideas for contents of additional chapters:

CHAPTER ITERATION VS RECURSION? or more generally CONTROL STRUCTURES 
references
Art of the interpreter, scheme, lambda
Friedman and Wise
lazy evaluator
Pratt
Michael Gordon, lit
Allen

Add section on iteration vs recursion.
    ex program that puts a program into iterative form where ever possible.?
Tail recursion
dynamic vs lexical binding (*function of maclisp)
dynamic and static binding - Sussman and Steele
cbv vs cbn
eval, neval, needeval, reval

continuations
Use of "continuations" for dynamic search
    --returns next item plus continuation describing how to restart the 
      search where it left off.

Backtracking  (would this be better in the section on control structures?)


CHAPTER PATTERN MATCHING, SYNTAX DIRECTED COMPUTATION

Syntax directed computation. 
	see SYNTAX.PUB[206,JMC]
    Compare to sd compiling  
    SDIO
XFORM functions, commutative and associative pattern matching.
production rules/control structure
theory? (semantics proof of correctness) not much known?
micro-PLANNER
Data driven programming: BB, Diffie compiler,
    Dispatch tables?

CHAPTER DIALECTS OF LISP, LISP SYSTEMS
?how relate to CONTROL STRUCTURES AND PM,SDC..?
LISP machine

CHAPTER APPLICATIONS?
macsyma and reduce


5. Applications to proof-checking and theorem proving.  This should
be the major application chapter.

CHAPTER METAPROGRAMS?

1. Programs that look at or produce programs.
e.g. is it iterative, compile maplists into functions,

APPENDIX: projects

Notes and comments.

See  LISP.NOT[E76,JMC]
     LISP.NOT[F77,JMC]
     LISP.2  [F77,JMC]


Interesting data structures.

Boolean expressions
Wffs, terms
proofs / derivations
grammars
machines
λ-expresions
LISP programs
Linear spaces and transformations
Ematch simpset (FOL)
Project and program ideas

Appendix containing substantial mathematical problem programmed in LISP.
	Card schuffling example  a shuffle is represented in the group
	algebra of S52 by sum prob(i)*perm(i).  Repeated schuffle rep by
	product.  How many schuffles required to make all perm equally
	probable?  Determined by eigenvalue of largest matrix in direct
	sum decomp of algebra.  Need to do more mathematics before this
	problem is finnishable on the computer.

Include some examples where the simplest Lisp programs are very bad:
	such as fib(n) = fib(n-1)+fib(n-2), or computing partitions of n
	via recusrive formula involving q(m,n) = those involving no more 
	than m numbers.  Consider solution using a table and keeping
	around only those values still needed in the table.

Boolean simplifier
tautology checker (Wang algorithm and truth table)
substitute into expressions with quantifiers
find the free variables
λ-conversion
unify
find and x st. (at various levels. this is the paradigm of a problem solver)
proof checker
proof strategy trier (interpreter)
problem solving strategy interpreter
PROGITER
make a function iterative
canonical forms of boolean and conditional expressions
simplify algebraic and lisp expressions
student helper:  program that analyses fndefinitions and point out possible
    errors (i) spelling errors, (ii) missing termination clause, (iii)
recursion not in a conditional, (iv) inconsistent operations on data
(eg adding to and cdring same data) (v) calls to undefined functions

Write search/successors in dynamic fashion so that a new position is
     position is generated only when required.  successors will need
     to remember where it is.  They could cooperate like co-routines.
     Compare the two programs for a variety of problems
     Extend technique to be used in the αβ search
     Generalize class of problems to which this sort of transformation
        is applicable.


Consider the problem of adding and deleting in a data structure in log k
time for the kth item.  How to do this in LISP, how to formalize proof in FOL.